/* Benchmarks for the PionterC verifier. */

// tree visit

struct tree
{
  int data;
  struct tree* left;
  struct tree* right;
};

/*@ let tree(t) =  (t==null) 
  @            || (({t}) && tree(t->left) && tree(t->right))
  @ in  tree(t)
  @ end
  @*/

int test_tree(struct tree* t)
{
  // body of function
  if (t==null)
    return 0;
  else
  return t->data;
}
/*@  */
